Theorem vtoclbg 3557

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 345	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3554	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-clel 2814

This theorem is referenced by:  alexeqg  3651  pm13.183  3666  elab6g  3669  elabgw  3679  sbc8g  3799  sbc2or  3800  sbccow  3814  sbcco  3817  sbc5ALT  3820  sbcie2g  3834  eqsbc1  3841  sbcng  3842  sbcimg  3843  sbcan  3844  sbcor  3845  sbcbig  3846  sbcal  3855  sbcex2  3856  sbcel1v  3862  sbcreu  3885  csbiebg  3941  sbcel12  4417  sbceqg  4418  csbie2df  4449  preq12bg  4858  elintrabg  4966  sbcbr123  5202  inisegn0  6119  fsn2g  7158  funfvima3  7256  elixpsn  8976  ixpsnf1o  8977  domeng  9002  1sdomOLD  9283  rankcf  10815  eldm3  35741  elima4  35757  brsset  35871  brbigcup  35880  elfix2  35886  elfunsg  35898  elsingles  35900  funpartlem  35924  ellines  36134  elhf2g  36158  bj-elpwgALT  37037  cover2g  37703  sbcrexgOLD  42773