Theorem vtoclbg 3533

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 348	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3531	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-clel 2844

This theorem is referenced by:  alexeqg  3619  pm13.183  3634  elab6g  3637  elabgw  3645  sbc8g  3761  sbc2or  3762  sbccow  3776  sbcco  3779  sbc5ALT  3782  sbcie2g  3793  eqsbc1  3799  sbcng  3800  sbcimg  3801  sbcan  3802  sbcor  3803  sbcbig  3804  sbcal  3812  sbcex2  3813  sbcel1v  3818  sbcreu  3838  csbiebg  3893  sbcel12  4382  sbceqg  4383  csbie2df  4414  preq12bg  4822  elintrabg  4930  sbcbr123  5169  inisegn0  6101  fsn2g  7135  funfvima3  7235  elixpsn  8934  ixpsnf1o  8935  domeng  8958  rankcf  10761  eldm3  36151  elima4  36166  brsset  36277  brbigcup  36286  elfix2  36292  elfunsg  36304  elsingles  36306  funpartlem  36332  ellines  36542  elhf2g  36566  bj-elpwgALT  37577  cover2g  38254